*****ASSUME ∀W.T(P,W);

1 ∀W.T(P,W)  (1)

*****∀E ↑ W1;

2 T(P,W1)  (1)

***** 2;

3 A(FOOL,W,W1)⊃T(P,W1)  (1)

*****∀I ↑ W1;

4 ∀W1.(A(FOOL,W,W1)⊃T(P,W1))  (1)

*****∀E KNOW FOOL,P,W;

5 T(K(FOOL,P),W)≡∀W1.(A(FOOL,W,W1)⊃T(P,W1))  

***** 4:5;

6 T(K(FOOL,P),W)  (1)

*****∀I ↑ W;

7 ∀W.T(K(FOOL,P),W)  (1)

*****⊃I 1⊃↑;

8 ∀W.T(P,W)⊃∀W.T(K(FOOL,P),W)  

*****ASSUME ∀W.T(K(FOOL,P),W);

9 ∀W.T(K(FOOL,P),W)  (9)

*****∀E ↑ W;

10 T(K(FOOL,P),W)  (9)

***** 5,10;

11 ∀W1.(A(FOOL,W,W1)⊃T(P,W1))  (9)

*****∀E ↑ W;

12 A(FOOL,W,W)⊃T(P,W)  (9)

*****∀E REFLEX FOOL,W;

13 A(FOOL,W,W)  

***** 12:13;

14 T(P,W)  (9)

*****∀I ↑ W;

15 ∀W.T(P,W)  (9)

*****⊃I 9⊃↑;

16 ∀W.T(K(FOOL,P),W)⊃∀W.T(P,W)  

***** 8,16;

17 ∀W.T(P,W)≡∀W.T(K(FOOL,P),W)  
*****LABEL (KNOWTAUT . 18);

*****∀I ↑ P;

18 ∀P.(∀W.T(P,W)≡∀W.T(K(FOOL,P),W))  

*****∀E IMP W,P,IMP(Q,P);

19 T(IMP(P,IMP(Q,P)),W)≡(T(P,W)⊃T(IMP(Q,P),W))  

*****∀E IMP W,Q,P;

20 T(IMP(Q,P),W)≡(T(Q,W)⊃T(P,W))  

***** 19:20;

21 T(IMP(P,IMP(Q,P)),W)  

*****∀I ↑ W;

22 ∀W.T(IMP(P,IMP(Q,P)),W)  

*****∀E 18 IMP(P,IMP(Q,P));

23 ∀W.T(IMP(P,IMP(Q,P)),W)≡∀W.T(K(FOOL,IMP(P,IMP(Q,P))),W)  

***** 22:23;

24 ∀W.T(K(FOOL,IMP(P,IMP(Q,P))),W)  

*****∀E ↑ W;

25 T(K(FOOL,IMP(P,IMP(Q,P))),W)  

*****∀I ↑ W P Q;

26 ∀W P Q.T(K(FOOL,IMP(P,IMP(Q,P))),W)